T:Type, ll:(T List) List, n:||concat(ll)||.
m:||ll||.
||concat(firstn(m;ll))||n
& n-||concat(firstn(m;ll))||<||ll[m]||
& concat(ll)[n] = ll[m][n-||concat(firstn(m;ll))||]  T 

latex

Definitions	Unit, P  Q, P  Q, T, , b, b, True, firstn(n;as), l[i], ij, i<j, hd(l), S  T, Top, Prop, SQType(T), {T}, ij, ||as||, as @ bs, Dec(P), P  Q, concat(ll), i  j < k, AB, P & Q, A, False, P  Q, x:A. B(x), A & B, {i..j}, x:A. B(x), t  T
Lemmas	int seg wf, length wf1, decidable lt, concat wf, append wf, length append, non neg length, le wf, select append front, top wf, first0, length cons, select wf, firstn wf, bnot wf, assert wf, le int wf, bool wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, select cons tl sq, select append back